[#14369] perf: normalize free variables in the type class resolution cache key by downstream-lean4[bot] · Pull Request #15 · leanprover/downstream-lean4

downstream-lean4 · 2026-07-24T14:27:57Z

This is the adaptation PR for leanprover/lean4#14369.

Kha · 2026-07-24T14:32:36Z

!bench mathlib

leanprover-radar · 2026-07-24T14:32:41Z

Benchmark results for 19e564b against 428f06e are in. There are significant results. @Kha

✅ build//instructions: -6.9T (-4.82%)

Large changes (52✅, 1🟥)

✅ build/module/Mathlib.Algebra.Group.Irreducible.Indecomposable//instructions: -7.6G (-20.43%)
✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -7.5G (-14.87%)
✅ build/module/Mathlib.Algebra.Order.ToIntervalMod//instructions: -19.8G (-27.21%)
✅ build/module/Mathlib.Algebra.Polynomial.RuleOfSigns//instructions: -12.2G (-25.82%)
✅ build/module/Mathlib.Algebra.Star.NonUnitalSubalgebra//instructions: -25.2G (-24.76%)
✅ build/module/Mathlib.Analysis.Analytic.Basic//instructions: -44.0G (-38.64%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -19.2G (-41.28%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomialDef//instructions: -19.0G (-40.21%)
✅ build/module/Mathlib.Analysis.Analytic.Constructions//instructions: -42.3G (-36.12%)
✅ build/module/Mathlib.Analysis.Analytic.ConvergenceRadius//instructions: -17.9G (-33.34%)
✅ build/module/Mathlib.Analysis.Asymptotics.TVS//instructions: -19.2G (-28.28%)
✅ build/module/Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity//instructions: -19.3G (-19.77%)
✅ build/module/Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances//instructions: -15.9G (-20.43%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Basic//instructions: -18.5G (-28.56%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Defs//instructions: -45.6G (-42.24%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries//instructions: -40.1G (-33.39%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Operations//instructions: -42.9G (-37.90%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Basic//instructions: -14.4G (-27.32%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Comp//instructions: -15.5G (-34.69%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Mul//instructions: -22.0G (-27.50%)
and 32 more
and 1 hidden

Medium changes (356✅, 1🟥)

✅ build/lakeprof/longest build path//instructions: -564.5G (-12.45%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalHom//instructions: -4.1G (-16.08%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -10.8G (-16.62%)
✅ build/module/Mathlib.Algebra.Algebra.Operations//instructions: -4.8G (-9.52%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Quasispectrum//instructions: -3.4G (-10.51%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Rank//instructions: -3.8G (-30.01%)
✅ build/module/Mathlib.Algebra.Algebra.Unitization//instructions: -5.6G (-12.29%)
✅ build/module/Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify//instructions: -5.4G (-10.70%)
✅ build/module/Mathlib.Algebra.DirectSum.Internal//instructions: -3.5G (-9.72%)
✅ build/module/Mathlib.Algebra.Exact.Basic//instructions: -2.7G (-7.07%)
✅ build/module/Mathlib.Algebra.FiveLemma//instructions: -3.2G (-15.53%)
✅ build/module/Mathlib.Algebra.Lie.Basis//instructions: -12.1G (-12.34%)
✅ build/module/Mathlib.Algebra.Lie.CartanExists//instructions: -3.6G (-11.66%)
✅ build/module/Mathlib.Algebra.Lie.Loop//instructions: -4.3G (-14.26%)
✅ build/module/Mathlib.Algebra.Lie.Submodule//instructions: -5.2G (-9.42%)
✅ build/module/Mathlib.Algebra.Lie.Weights.Cartan//instructions: -3.9G (-11.12%)
✅ build/module/Mathlib.Algebra.Lie.Weights.IsSimple//instructions: -4.5G (-6.62%)
✅ build/module/Mathlib.Algebra.Lie.Weights.Killing//instructions: -8.8G (-10.90%)
✅ build/module/Mathlib.Algebra.Lie.Weights.RootSystem//instructions: -7.8G (-12.57%)
✅ build/module/Mathlib.Algebra.Module.Injective//instructions: -3.5G (-11.45%)
and 337 more

Small changes (1047✅, 6🟥)

✅ build/module/Aesop.Saturate//instructions: -571.4M (-3.98%)
✅ build/module/Aesop.Script.SpecificTactics//instructions: -791.5M (-9.12%)
✅ build/module/Aesop.Search.Expansion.Norm//instructions: -498.7M (-3.90%)
✅ build/module/Aesop.Search.Main//instructions: -404.5M (-4.01%)
✅ build/module/Aesop.Tree.ExtractScript//instructions: -425.0M (-7.48%)
✅ build/module/Batteries.Data.List.Lemmas//instructions: -1.6G (-3.95%)
✅ build/module/Batteries.Tactic.GeneralizeProofs//instructions: -406.0M (-3.39%)
✅ build/module/Mathlib.Algebra.AddConstMap.Basic//instructions: -1.9G (-8.10%)
✅ build/module/Mathlib.Algebra.Algebra.Bilinear//instructions: -2.0G (-12.95%)
✅ build/module/Mathlib.Algebra.Algebra.Equiv//instructions: -1.6G (-4.16%)
✅ build/module/Mathlib.Algebra.Algebra.Hom//instructions: -700.3M (-3.60%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Basic//instructions: -1.5G (-5.85%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Lattice//instructions: -1.2G (-3.03%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Unitization//instructions: -1.5G (-6.80%)
✅ build/module/Mathlib.Algebra.Algebra.Tower//instructions: -1.3G (-6.59%)
✅ build/module/Mathlib.Algebra.Azumaya.Matrix//instructions: -1.4G (-8.77%)
✅ build/module/Mathlib.Algebra.BigOperators.Expect//instructions: -1.2G (-6.27%)
✅ build/module/Mathlib.Algebra.BigOperators.Fin//instructions: -3.2G (-6.52%)
✅ build/module/Mathlib.Algebra.BigOperators.Finprod//instructions: -2.8G (-5.62%)
✅ build/module/Mathlib.Algebra.BigOperators.Finsupp.Basic//instructions: -1.9G (-6.91%)
and 1033 more

leanprover-radar · 2026-07-24T14:32:44Z

This command can only be used in the lean4 repository.

_{You can edit the original message until the command succeeds.}

downstream-lean4 · 2026-07-24T15:58:56Z

Build report for downstream: follow upstream PR

Turned red:

Repo	Critical	Build	Test	Lint
aesop	✅	✅ in 19s	🟥 in 5s	⏭️
mathlib4	✅	🟥 in 7s	⏭️	⏭️
cslib		⏭️	⏭️	⏭️
lean4export		✅ in 3s	🟥 in 7s	⏭️

Stayed red

Repo	Critical	Build	Test	Lint
verso-slides		🟥 in 22s	⏭️	⏭️

Stayed green

Repo	Critical	Build	Test	Lint
batteries	✅	✅ in 15s	✅ in 4s	✅ in 1s
import-graph	✅	✅ in 3s	✅ in 3s	⏭️
lean4-cli	✅	✅ in 4s	✅ in 0s	⏭️
plausible	✅	✅ in 4s	✅ in 2s	⏭️
ProofWidgets4	✅	✅ in 4s	✅ in 1s	⏭️
quote4	✅	✅ in 6s	✅ in 1s	⏭️
reference-manual	✅	✅ in 81s	⏭️	⏭️
BibtexQuery		✅ in 3s	⏭️	⏭️
comparator		✅ in 3s	⏭️	⏭️
doc-gen4		✅ in 15s	⏭️	⏭️
illuminate		✅ in 8s	✅ in 11s	⏭️
lean4-unicode-basic		✅ in 4s	✅ in 9s	⏭️
LeanSearchClient		✅ in 2s	✅ in 0s	⏭️
leansqlite		✅ in 10s	✅ in 20s	⏭️
repl		✅ in 4s	✅ in 18s	⏭️
verso		✅ in 98s	✅ in 78s	⏭️
verso-web-components		✅ in 8s	⏭️	⏭️

View run

Kha · 2026-07-24T17:59:57Z

!bench mathlib

leanprover-radar · 2026-07-24T18:01:35Z

Benchmark results for f519b24 against 428f06e are in. There are significant results. @Kha

✅ build//instructions: -5.6T (-3.88%)

Large changes (35✅, 1🟥)

✅ build/module/Mathlib.Algebra.Group.Irreducible.Indecomposable//instructions: -7.4G (-20.08%)
✅ build/module/Mathlib.Algebra.Order.ToIntervalMod//instructions: -16.6G (-22.72%)
✅ build/module/Mathlib.Algebra.Star.NonUnitalSubalgebra//instructions: -25.2G (-24.71%)
✅ build/module/Mathlib.Analysis.Analytic.Basic//instructions: -39.8G (-35.02%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -17.2G (-37.08%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomialDef//instructions: -17.9G (-37.79%)
✅ build/module/Mathlib.Analysis.Analytic.Constructions//instructions: -39.5G (-33.66%)
✅ build/module/Mathlib.Analysis.Analytic.ConvergenceRadius//instructions: -17.4G (-32.34%)
✅ build/module/Mathlib.Analysis.Asymptotics.TVS//instructions: -16.7G (-24.61%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Basic//instructions: -15.9G (-24.48%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Defs//instructions: -40.0G (-37.06%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries//instructions: -34.3G (-28.56%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Operations//instructions: -40.0G (-35.33%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Mul//instructions: -17.0G (-21.21%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Add//instructions: -21.1G (-28.71%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.CompCLM//instructions: -25.3G (-33.84%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Equiv//instructions: -13.2G (-23.41%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Mul//instructions: -26.3G (-19.42%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Prod//instructions: -28.2G (-34.63%)
✅ build/module/Mathlib.Analysis.Calculus.FormalMultilinearSeries//instructions: -10.3G (-24.84%)
and 15 more
and 1 hidden

Medium changes (255✅, 1🟥)

✅ build/module/Mathlib.Algebra.Algebra.NonUnitalHom//instructions: -3.9G (-15.19%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -10.5G (-16.10%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Quasispectrum//instructions: -3.1G (-9.64%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Rank//instructions: -3.8G (-30.21%)
✅ build/module/Mathlib.Algebra.Algebra.Unitization//instructions: -5.5G (-12.16%)
✅ build/module/Mathlib.Algebra.Exact.Basic//instructions: -2.6G (-6.89%)
✅ build/module/Mathlib.Algebra.FiveLemma//instructions: -3.0G (-14.62%)
✅ build/module/Mathlib.Algebra.Lie.Basis//instructions: -12.3G (-12.45%)
✅ build/module/Mathlib.Algebra.Lie.CartanExists//instructions: -3.2G (-10.66%)
✅ build/module/Mathlib.Algebra.Lie.Loop//instructions: -4.2G (-13.66%)
✅ build/module/Mathlib.Algebra.Lie.Submodule//instructions: -4.4G (-7.92%)
✅ build/module/Mathlib.Algebra.Lie.Weights.Cartan//instructions: -3.6G (-10.46%)
✅ build/module/Mathlib.Algebra.Lie.Weights.RootSystem//instructions: -6.4G (-10.31%)
✅ build/module/Mathlib.Algebra.Module.Injective//instructions: -3.3G (-10.75%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Defs//instructions: -2.4G (-5.22%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Polynomial//instructions: -4.7G (-12.34%)
✅ build/module/Mathlib.Algebra.Module.LocalizedModule.Submodule//instructions: -3.2G (-8.25%)
✅ build/module/Mathlib.Algebra.Module.SnakeLemma//instructions: -2.5G (-15.09%)
✅ build/module/Mathlib.Algebra.Module.ZLattice.Summable//instructions: -4.9G (-10.69%)
✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -2.9G (-5.69%)
and 236 more

Small changes (840✅, 6🟥)

✅ build/lakeprof/longest build path//instructions: -523.9G (-11.56%)
✅ build/module/Aesop.Saturate//instructions: -568.9M (-3.96%)
✅ build/module/Aesop.Script.SpecificTactics//instructions: -838.0M (-9.65%)
✅ build/module/Aesop.Search.Expansion.Norm//instructions: -514.1M (-4.02%)
✅ build/module/Aesop.Search.Main//instructions: -415.0M (-4.12%)
✅ build/module/Aesop.Tree.ExtractScript//instructions: -437.0M (-7.69%)
✅ build/module/Batteries.Tactic.GeneralizeProofs//instructions: -425.3M (-3.55%)
✅ build/module/Mathlib.Algebra.AddConstMap.Basic//instructions: -1.7G (-7.26%)
✅ build/module/Mathlib.Algebra.Algebra.Bilinear//instructions: -2.0G (-13.10%)
✅ build/module/Mathlib.Algebra.Algebra.Equiv//instructions: -1.5G (-3.78%)
✅ build/module/Mathlib.Algebra.Algebra.Hom//instructions: -694.3M (-3.57%)
✅ build/module/Mathlib.Algebra.Algebra.Operations//instructions: -4.0G (-7.88%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Basic//instructions: -1.2G (-4.85%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Unitization//instructions: -1.3G (-6.21%)
✅ build/module/Mathlib.Algebra.Algebra.Tower//instructions: -1.3G (-6.54%)
✅ build/module/Mathlib.Algebra.Azumaya.Matrix//instructions: -1.5G (-9.38%)
✅ build/module/Mathlib.Algebra.BigOperators.Expect//instructions: -877.1M (-4.41%)
✅ build/module/Mathlib.Algebra.BigOperators.Fin//instructions: -1.8G (-3.64%)
✅ build/module/Mathlib.Algebra.BigOperators.Finprod//instructions: -1.6G (-3.30%)
✅ build/module/Mathlib.Algebra.BigOperators.Finsupp.Basic//instructions: -1.9G (-6.89%)
and 826 more

Kha · 2026-07-26T13:20:55Z

!bench mathlib

leanprover-radar · 2026-07-26T13:22:16Z

Benchmark results for 73ebb47 against 428f06e are in. There are significant results. @Kha

✅ build//instructions: -5.4T (-3.77%)

Large changes (35✅, 1🟥)

✅ build/module/Mathlib.Algebra.Group.Irreducible.Indecomposable//instructions: -7.3G (-19.82%)
✅ build/module/Mathlib.Algebra.Order.ToIntervalMod//instructions: -16.1G (-22.11%)
✅ build/module/Mathlib.Algebra.Star.NonUnitalSubalgebra//instructions: -24.8G (-24.37%)
✅ build/module/Mathlib.Analysis.Analytic.Basic//instructions: -39.2G (-34.45%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -17.1G (-36.77%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomialDef//instructions: -17.3G (-36.61%)
✅ build/module/Mathlib.Analysis.Analytic.Constructions//instructions: -39.3G (-33.50%)
✅ build/module/Mathlib.Analysis.Analytic.ConvergenceRadius//instructions: -16.9G (-31.52%)
✅ build/module/Mathlib.Analysis.Asymptotics.TVS//instructions: -16.5G (-24.39%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Basic//instructions: -15.3G (-23.66%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Defs//instructions: -39.7G (-36.81%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries//instructions: -32.0G (-26.59%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Operations//instructions: -39.8G (-35.18%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Mul//instructions: -16.5G (-20.70%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Add//instructions: -20.2G (-27.55%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.CompCLM//instructions: -24.4G (-32.69%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Equiv//instructions: -12.7G (-22.39%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Mul//instructions: -25.9G (-19.07%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Prod//instructions: -27.8G (-34.15%)
✅ build/module/Mathlib.Analysis.Calculus.FormalMultilinearSeries//instructions: -10.0G (-23.99%)
and 15 more
and 1 hidden

Medium changes (223✅, 2🟥)

✅ build/module/Mathlib.Algebra.Algebra.NonUnitalHom//instructions: -3.9G (-15.17%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -10.2G (-15.75%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Quasispectrum//instructions: -3.0G (-9.41%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Rank//instructions: -3.8G (-30.07%)
✅ build/module/Mathlib.Algebra.Algebra.Unitization//instructions: -5.4G (-11.91%)
✅ build/module/Mathlib.Algebra.Exact.Basic//instructions: -2.5G (-6.56%)
✅ build/module/Mathlib.Algebra.FiveLemma//instructions: -3.0G (-14.74%)
✅ build/module/Mathlib.Algebra.Lie.Basis//instructions: -12.0G (-12.19%)
✅ build/module/Mathlib.Algebra.Lie.Loop//instructions: -4.2G (-13.65%)
✅ build/module/Mathlib.Algebra.Lie.Weights.RootSystem//instructions: -5.4G (-8.73%)
✅ build/module/Mathlib.Algebra.Module.Injective//instructions: -2.8G (-9.20%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Polynomial//instructions: -4.6G (-12.03%)
✅ build/module/Mathlib.Algebra.Module.LocalizedModule.Submodule//instructions: -3.0G (-7.81%)
✅ build/module/Mathlib.Algebra.Module.SnakeLemma//instructions: -2.5G (-15.23%)
✅ build/module/Mathlib.Algebra.Module.ZLattice.Summable//instructions: -4.7G (-10.23%)
✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -2.6G (-5.25%)
✅ build/module/Mathlib.Algebra.Order.Module.HahnEmbedding//instructions: -11.5G (-12.00%)
✅ build/module/Mathlib.Algebra.Order.Rearrangement//instructions: -3.0G (-13.36%)
✅ build/module/Mathlib.Algebra.Polynomial.Module.Basic//instructions: -5.7G (-13.93%)
✅ build/module/Mathlib.Algebra.Polynomial.RuleOfSigns//instructions: -10.0G (-21.19%)
and 205 more

Small changes (817✅, 7🟥)

✅ build/lakeprof/longest build path//instructions: -539.2G (-11.89%)
✅ build/module/Aesop.Saturate//instructions: -539.2M (-3.76%)
✅ build/module/Aesop.Script.SpecificTactics//instructions: -810.2M (-9.33%)
✅ build/module/Aesop.Search.Expansion.Norm//instructions: -498.2M (-3.89%)
✅ build/module/Aesop.Search.Main//instructions: -397.0M (-3.94%)
✅ build/module/Aesop.Tree.ExtractScript//instructions: -418.9M (-7.37%)
✅ build/module/Batteries.Tactic.GeneralizeProofs//instructions: -402.5M (-3.36%)
✅ build/module/Mathlib.Algebra.AddConstMap.Basic//instructions: -1.6G (-6.63%)
✅ build/module/Mathlib.Algebra.Algebra.Bilinear//instructions: -2.0G (-12.85%)
✅ build/module/Mathlib.Algebra.Algebra.Equiv//instructions: -1.4G (-3.61%)
✅ build/module/Mathlib.Algebra.Algebra.Operations//instructions: -3.7G (-7.31%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Basic//instructions: -1.1G (-4.48%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Unitization//instructions: -1.3G (-6.14%)
✅ build/module/Mathlib.Algebra.Algebra.Tower//instructions: -1.3G (-6.18%)
✅ build/module/Mathlib.Algebra.BigOperators.Fin//instructions: -1.5G (-3.05%)
✅ build/module/Mathlib.Algebra.BigOperators.Finprod//instructions: -1.6G (-3.25%)
✅ build/module/Mathlib.Algebra.BigOperators.Finsupp.Basic//instructions: -1.9G (-6.78%)
✅ build/module/Mathlib.Algebra.BigOperators.Group.Finset.Basic//instructions: -1.0G (-2.14%)
✅ build/module/Mathlib.Algebra.Category.CommAlgCat.Monoidal//instructions: -2.1G (-2.72%)
✅ build/module/Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf//instructions: -1.8G (-5.69%)
and 804 more

Kha · 2026-07-26T15:12:30Z

!bench mathlib

leanprover-radar · 2026-07-26T15:13:47Z

Benchmark results for c1515c8 against 428f06e are in. There are significant results. @Kha

✅ build//instructions: -5.6T (-3.87%)

Large changes (34✅)

✅ build/module/Mathlib.Algebra.Group.Irreducible.Indecomposable//instructions: -7.4G (-19.90%)
✅ build/module/Mathlib.Algebra.Order.ToIntervalMod//instructions: -16.2G (-22.26%)
✅ build/module/Mathlib.Algebra.Star.NonUnitalSubalgebra//instructions: -25.0G (-24.56%)
✅ build/module/Mathlib.Analysis.Analytic.Basic//instructions: -39.2G (-34.45%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -17.3G (-37.13%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomialDef//instructions: -17.5G (-36.90%)
✅ build/module/Mathlib.Analysis.Analytic.Constructions//instructions: -39.4G (-33.61%)
✅ build/module/Mathlib.Analysis.Analytic.ConvergenceRadius//instructions: -17.1G (-31.81%)
✅ build/module/Mathlib.Analysis.Asymptotics.TVS//instructions: -16.7G (-24.58%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Basic//instructions: -15.3G (-23.58%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Defs//instructions: -39.8G (-36.89%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries//instructions: -32.0G (-26.63%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Operations//instructions: -39.9G (-35.26%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Mul//instructions: -16.7G (-20.85%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Add//instructions: -20.5G (-27.93%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.CompCLM//instructions: -24.8G (-33.10%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Equiv//instructions: -12.8G (-22.63%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Mul//instructions: -26.2G (-19.32%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Prod//instructions: -28.1G (-34.47%)
✅ build/module/Mathlib.Analysis.Calculus.FormalMultilinearSeries//instructions: -10.0G (-24.01%)
and 13 more
and 1 hidden

Medium changes (234✅, 1🟥)

✅ build/module/Mathlib.Algebra.Algebra.NonUnitalHom//instructions: -3.9G (-15.27%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -10.4G (-15.92%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Quasispectrum//instructions: -3.0G (-9.49%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Rank//instructions: -3.7G (-29.95%)
✅ build/module/Mathlib.Algebra.Algebra.Unitization//instructions: -5.5G (-12.20%)
✅ build/module/Mathlib.Algebra.Exact.Basic//instructions: -2.5G (-6.67%)
✅ build/module/Mathlib.Algebra.FiveLemma//instructions: -3.1G (-15.24%)
✅ build/module/Mathlib.Algebra.Lie.Basis//instructions: -12.5G (-12.70%)
✅ build/module/Mathlib.Algebra.Lie.Loop//instructions: -4.2G (-13.73%)
✅ build/module/Mathlib.Algebra.Lie.Weights.Cartan//instructions: -3.6G (-10.32%)
✅ build/module/Mathlib.Algebra.Lie.Weights.RootSystem//instructions: -5.6G (-9.04%)
✅ build/module/Mathlib.Algebra.Module.Injective//instructions: -2.9G (-9.32%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Defs//instructions: -2.3G (-5.05%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Polynomial//instructions: -4.7G (-12.23%)
✅ build/module/Mathlib.Algebra.Module.LocalizedModule.Submodule//instructions: -3.1G (-8.05%)
✅ build/module/Mathlib.Algebra.Module.SnakeLemma//instructions: -2.6G (-15.62%)
✅ build/module/Mathlib.Algebra.Module.ZLattice.Summable//instructions: -4.7G (-10.39%)
✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -2.7G (-5.39%)
✅ build/module/Mathlib.Algebra.Order.Module.HahnEmbedding//instructions: -11.8G (-12.24%)
✅ build/module/Mathlib.Algebra.Order.Rearrangement//instructions: -3.1G (-13.96%)
and 215 more

Small changes (830✅, 6🟥)

✅ build/lakeprof/longest build path//instructions: -517.5G (-11.42%)
✅ build/module/Aesop.Saturate//instructions: -540.1M (-3.76%)
✅ build/module/Aesop.Script.SpecificTactics//instructions: -810.2M (-9.33%)
✅ build/module/Aesop.Search.Expansion.Norm//instructions: -493.2M (-3.86%)
✅ build/module/Aesop.Search.Main//instructions: -402.1M (-3.99%)
✅ build/module/Aesop.Tree.ExtractScript//instructions: -418.6M (-7.37%)
✅ build/module/Batteries.Tactic.GeneralizeProofs//instructions: -401.4M (-3.35%)
✅ build/module/Mathlib.Algebra.AddConstMap.Basic//instructions: -1.6G (-6.87%)
✅ build/module/Mathlib.Algebra.Algebra.Bilinear//instructions: -2.0G (-12.97%)
✅ build/module/Mathlib.Algebra.Algebra.Equiv//instructions: -1.5G (-3.71%)
✅ build/module/Mathlib.Algebra.Algebra.Operations//instructions: -4.0G (-7.87%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Basic//instructions: -1.1G (-4.50%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Unitization//instructions: -1.3G (-6.19%)
✅ build/module/Mathlib.Algebra.Algebra.Tower//instructions: -1.3G (-6.25%)
✅ build/module/Mathlib.Algebra.BigOperators.Fin//instructions: -1.5G (-3.10%)
✅ build/module/Mathlib.Algebra.BigOperators.Finprod//instructions: -1.6G (-3.19%)
✅ build/module/Mathlib.Algebra.BigOperators.Finsupp.Basic//instructions: -1.7G (-6.33%)
✅ build/module/Mathlib.Algebra.BigOperators.Group.Finset.Basic//instructions: -1.0G (-2.20%)
✅ build/module/Mathlib.Algebra.Category.CommAlgCat.Monoidal//instructions: -2.1G (-2.76%)
✅ build/module/Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf//instructions: -1.7G (-5.53%)
and 816 more

Kha · 2026-07-28T08:18:21Z

!bench mathlib

leanprover-radar · 2026-07-28T08:18:52Z

Benchmark results for e0da297 against 428f06e are in. There are significant results. @Kha

✅ build//instructions: -5.5T (-3.83%)

Large changes (35✅)

✅ build/module/Mathlib.Algebra.Group.Irreducible.Indecomposable//instructions: -7.4G (-19.95%)
✅ build/module/Mathlib.Algebra.Order.ToIntervalMod//instructions: -16.1G (-22.13%)
✅ build/module/Mathlib.Algebra.Star.NonUnitalSubalgebra//instructions: -25.0G (-24.56%)
✅ build/module/Mathlib.Analysis.Analytic.Basic//instructions: -39.3G (-34.51%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -17.2G (-37.05%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomialDef//instructions: -17.5G (-36.89%)
✅ build/module/Mathlib.Analysis.Analytic.Constructions//instructions: -39.4G (-33.63%)
✅ build/module/Mathlib.Analysis.Analytic.ConvergenceRadius//instructions: -17.1G (-31.73%)
✅ build/module/Mathlib.Analysis.Asymptotics.TVS//instructions: -16.6G (-24.55%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Basic//instructions: -15.4G (-23.72%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Defs//instructions: -39.8G (-36.87%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries//instructions: -32.1G (-26.66%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Operations//instructions: -40.0G (-35.30%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Mul//instructions: -16.7G (-20.93%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Add//instructions: -20.5G (-27.93%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.CompCLM//instructions: -24.7G (-33.06%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap//instructions: -13.2G (-20.25%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Equiv//instructions: -12.8G (-22.61%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Mul//instructions: -26.2G (-19.35%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Prod//instructions: -28.0G (-34.43%)
and 14 more
and 1 hidden

Medium changes (237✅, 1🟥)

✅ build/module/Mathlib.Algebra.Algebra.NonUnitalHom//instructions: -3.9G (-15.26%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -10.4G (-15.92%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Quasispectrum//instructions: -3.1G (-9.56%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Rank//instructions: -3.8G (-30.06%)
✅ build/module/Mathlib.Algebra.Algebra.Unitization//instructions: -5.5G (-12.20%)
✅ build/module/Mathlib.Algebra.Exact.Basic//instructions: -2.6G (-6.76%)
✅ build/module/Mathlib.Algebra.FiveLemma//instructions: -3.1G (-15.18%)
✅ build/module/Mathlib.Algebra.Lie.Basis//instructions: -12.5G (-12.71%)
✅ build/module/Mathlib.Algebra.Lie.Loop//instructions: -4.2G (-13.79%)
✅ build/module/Mathlib.Algebra.Lie.Weights.RootSystem//instructions: -5.6G (-9.14%)
✅ build/module/Mathlib.Algebra.Module.Injective//instructions: -2.9G (-9.30%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Defs//instructions: -2.3G (-5.05%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Polynomial//instructions: -4.6G (-12.12%)
✅ build/module/Mathlib.Algebra.Module.LocalizedModule.Basic//instructions: -7.1G (-7.39%)
✅ build/module/Mathlib.Algebra.Module.LocalizedModule.Submodule//instructions: -3.1G (-8.04%)
✅ build/module/Mathlib.Algebra.Module.SnakeLemma//instructions: -2.6G (-15.54%)
✅ build/module/Mathlib.Algebra.Module.ZLattice.Summable//instructions: -4.7G (-10.40%)
✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -2.6G (-5.20%)
✅ build/module/Mathlib.Algebra.Order.Module.HahnEmbedding//instructions: -11.7G (-12.20%)
✅ build/module/Mathlib.Algebra.Order.Rearrangement//instructions: -3.1G (-14.02%)
and 218 more

Small changes (822✅, 6🟥)

✅ build/lakeprof/longest build path//instructions: -511.9G (-11.29%)
✅ build/module/Aesop.Saturate//instructions: -544.1M (-3.79%)
✅ build/module/Aesop.Script.SpecificTactics//instructions: -809.7M (-9.33%)
✅ build/module/Aesop.Search.Expansion.Norm//instructions: -497.5M (-3.89%)
✅ build/module/Aesop.Search.Main//instructions: -405.3M (-4.02%)
✅ build/module/Aesop.Tree.ExtractScript//instructions: -419.9M (-7.39%)
✅ build/module/Batteries.Tactic.GeneralizeProofs//instructions: -403.5M (-3.37%)
✅ build/module/Mathlib.Algebra.AddConstMap.Basic//instructions: -1.6G (-6.76%)
✅ build/module/Mathlib.Algebra.Algebra.Bilinear//instructions: -2.0G (-13.11%)
✅ build/module/Mathlib.Algebra.Algebra.Equiv//instructions: -1.5G (-3.75%)
✅ build/module/Mathlib.Algebra.Algebra.Operations//instructions: -3.9G (-7.73%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Basic//instructions: -1.1G (-4.51%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Unitization//instructions: -1.3G (-6.14%)
✅ build/module/Mathlib.Algebra.Algebra.Tower//instructions: -1.3G (-6.31%)
✅ build/module/Mathlib.Algebra.BigOperators.Fin//instructions: -1.5G (-3.06%)
✅ build/module/Mathlib.Algebra.BigOperators.Finprod//instructions: -1.6G (-3.25%)
✅ build/module/Mathlib.Algebra.BigOperators.Finsupp.Basic//instructions: -1.8G (-6.46%)
✅ build/module/Mathlib.Algebra.BigOperators.Group.Finset.Basic//instructions: -1.1G (-2.22%)
✅ build/module/Mathlib.Algebra.Category.CommAlgCat.Monoidal//instructions: -2.1G (-2.70%)
✅ build/module/Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf//instructions: -1.7G (-5.50%)
and 808 more

Kha · 2026-07-28T16:57:02Z

!bench mathlib

leanprover-radar · 2026-07-28T16:57:39Z

Benchmark results for 4eb9917 against 428f06e are in. There are significant results. @Kha

✅ build//instructions: -5.3T (-3.69%)

Large changes (38✅)

✅ build/module/Mathlib.Algebra.Group.Irreducible.Indecomposable//instructions: -7.3G (-19.85%)
✅ build/module/Mathlib.Algebra.Order.ToIntervalMod//instructions: -16.1G (-22.06%)
✅ build/module/Mathlib.Algebra.Star.NonUnitalSubalgebra//instructions: -24.9G (-24.47%)
✅ build/module/Mathlib.Analysis.Analytic.Basic//instructions: -39.2G (-34.46%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -17.2G (-37.06%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomialDef//instructions: -17.4G (-36.75%)
✅ build/module/Mathlib.Analysis.Analytic.Constructions//instructions: -39.3G (-33.56%)
✅ build/module/Mathlib.Analysis.Analytic.ConvergenceRadius//instructions: -17.0G (-31.65%)
✅ build/module/Mathlib.Analysis.Asymptotics.TVS//instructions: -16.6G (-24.49%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Basic//instructions: -15.3G (-23.57%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Defs//instructions: -39.7G (-36.77%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries//instructions: -31.8G (-26.47%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Operations//instructions: -39.8G (-35.17%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Mul//instructions: -16.6G (-20.74%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Prod//instructions: -9.5G (-42.36%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Add//instructions: -20.4G (-27.83%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.CompCLM//instructions: -24.7G (-33.00%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap//instructions: -13.2G (-20.17%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Equiv//instructions: -12.7G (-22.49%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Mul//instructions: -26.0G (-19.14%)
and 17 more
and 1 hidden

Medium changes (230✅, 1🟥)

✅ build/module/Mathlib.Algebra.Algebra.NonUnitalHom//instructions: -3.9G (-15.16%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -10.3G (-15.79%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Quasispectrum//instructions: -3.0G (-9.39%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Rank//instructions: -3.7G (-29.79%)
✅ build/module/Mathlib.Algebra.Algebra.Unitization//instructions: -5.4G (-12.03%)
✅ build/module/Mathlib.Algebra.Exact.Basic//instructions: -2.5G (-6.67%)
✅ build/module/Mathlib.Algebra.FiveLemma//instructions: -3.1G (-15.05%)
✅ build/module/Mathlib.Algebra.Lie.Basis//instructions: -12.4G (-12.56%)
✅ build/module/Mathlib.Algebra.Lie.Loop//instructions: -4.2G (-13.75%)
✅ build/module/Mathlib.Algebra.Lie.Weights.RootSystem//instructions: -5.5G (-8.95%)
✅ build/module/Mathlib.Algebra.Module.Injective//instructions: -2.8G (-9.22%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Polynomial//instructions: -4.6G (-12.01%)
✅ build/module/Mathlib.Algebra.Module.LocalizedModule.Basic//instructions: -7.0G (-7.25%)
✅ build/module/Mathlib.Algebra.Module.LocalizedModule.Submodule//instructions: -3.0G (-7.90%)
✅ build/module/Mathlib.Algebra.Module.SnakeLemma//instructions: -2.5G (-15.39%)
✅ build/module/Mathlib.Algebra.Module.ZLattice.Summable//instructions: -4.7G (-10.26%)
✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -2.6G (-5.10%)
✅ build/module/Mathlib.Algebra.Order.Module.HahnEmbedding//instructions: -11.7G (-12.14%)
✅ build/module/Mathlib.Algebra.Order.Rearrangement//instructions: -2.9G (-13.10%)
✅ build/module/Mathlib.Algebra.Polynomial.Module.Basic//instructions: -5.7G (-13.97%)
and 211 more

Small changes (803✅, 7🟥)

✅ build/lakeprof/longest build path//instructions: -503.5G (-11.11%)
✅ build/module/Aesop.Saturate//instructions: -523.2M (-3.65%)
✅ build/module/Aesop.Script.SpecificTactics//instructions: -796.8M (-9.18%)
✅ build/module/Aesop.Search.Expansion.Norm//instructions: -428.5M (-3.35%)
✅ build/module/Aesop.Search.Main//instructions: -344.7M (-3.42%)
✅ build/module/Aesop.Tree.ExtractScript//instructions: -404.8M (-7.13%)
✅ build/module/Mathlib.Algebra.AddConstMap.Basic//instructions: -1.6G (-6.72%)
✅ build/module/Mathlib.Algebra.Algebra.Bilinear//instructions: -2.0G (-12.79%)
✅ build/module/Mathlib.Algebra.Algebra.Equiv//instructions: -1.4G (-3.64%)
✅ build/module/Mathlib.Algebra.Algebra.Operations//instructions: -3.7G (-7.43%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Unitization//instructions: -1.3G (-5.95%)
✅ build/module/Mathlib.Algebra.Algebra.Tower//instructions: -1.3G (-6.30%)
✅ build/module/Mathlib.Algebra.BigOperators.Fin//instructions: -1.4G (-2.77%)
✅ build/module/Mathlib.Algebra.BigOperators.Finprod//instructions: -1.6G (-3.14%)
✅ build/module/Mathlib.Algebra.BigOperators.Finsupp.Basic//instructions: -1.8G (-6.61%)
✅ build/module/Mathlib.Algebra.BigOperators.Group.Finset.Basic//instructions: -965.1M (-2.04%)
✅ build/module/Mathlib.Algebra.Category.CommAlgCat.Monoidal//instructions: -2.1G (-2.69%)
✅ build/module/Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf//instructions: -1.7G (-5.53%)
✅ build/module/Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic//instructions: -2.0G (-5.61%)
✅ build/module/Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify//instructions: -2.5G (-4.92%)
and 790 more

Garmelon · 2026-07-28T17:31:19Z

!bench cslib

leanprover-radar · 2026-07-28T17:31:37Z

Waiting until the labels cache-available toolchain-available are added.

_{You can edit the original message until the command succeeds.}

Garmelon · 2026-07-28T20:12:28Z

Ah, this PR is from before I updated the caching logic. To test !bench cslib properly in this PR, you should merge green (and merge downstream-green at the same time in the upstream PR).

Kha · 2026-07-29T16:53:29Z

!bench mathlib

leanprover-radar · 2026-07-29T16:54:50Z

Benchmark results for de38a79 against 428f06e are in. There are significant results. @Kha

✅ build//instructions: -5.6T (-3.90%)

Large changes (42✅)

✅ build/module/Mathlib.Algebra.Group.Irreducible.Indecomposable//instructions: -7.3G (-19.62%)
✅ build/module/Mathlib.Algebra.Order.ToIntervalMod//instructions: -16.5G (-22.57%)
✅ build/module/Mathlib.Algebra.Polynomial.RuleOfSigns//instructions: -10.1G (-21.41%)
✅ build/module/Mathlib.Algebra.Star.NonUnitalSubalgebra//instructions: -25.2G (-24.74%)
✅ build/module/Mathlib.Analysis.Analytic.Basic//instructions: -39.7G (-34.90%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -17.3G (-37.28%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomialDef//instructions: -17.9G (-37.80%)
✅ build/module/Mathlib.Analysis.Analytic.Constructions//instructions: -39.5G (-33.69%)
✅ build/module/Mathlib.Analysis.Analytic.ConvergenceRadius//instructions: -17.4G (-32.33%)
✅ build/module/Mathlib.Analysis.Asymptotics.TVS//instructions: -16.7G (-24.62%)
✅ build/module/Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity//instructions: -17.6G (-17.98%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Basic//instructions: -16.0G (-24.66%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Defs//instructions: -39.9G (-36.94%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries//instructions: -34.2G (-28.48%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Operations//instructions: -40.1G (-35.39%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Mul//instructions: -17.1G (-21.35%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Add//instructions: -21.3G (-28.96%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Analytic//instructions: -25.0G (-20.98%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Basic//instructions: -16.0G (-26.33%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.CompCLM//instructions: -25.5G (-34.09%)
and 21 more
and 1 hidden

Medium changes (255✅, 1🟥)

✅ build/module/Mathlib.Algebra.Algebra.NonUnitalHom//instructions: -3.9G (-15.22%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -10.5G (-16.16%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Quasispectrum//instructions: -3.1G (-9.68%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Rank//instructions: -3.8G (-30.03%)
✅ build/module/Mathlib.Algebra.Algebra.Unitization//instructions: -5.5G (-12.13%)
✅ build/module/Mathlib.Algebra.Exact.Basic//instructions: -2.6G (-6.93%)
✅ build/module/Mathlib.Algebra.FiveLemma//instructions: -3.1G (-15.30%)
✅ build/module/Mathlib.Algebra.Lie.Basis//instructions: -12.4G (-12.59%)
✅ build/module/Mathlib.Algebra.Lie.CartanExists//instructions: -3.2G (-10.60%)
✅ build/module/Mathlib.Algebra.Lie.Loop//instructions: -4.2G (-13.83%)
✅ build/module/Mathlib.Algebra.Lie.Weights.Cartan//instructions: -3.7G (-10.70%)
✅ build/module/Mathlib.Algebra.Lie.Weights.IsSimple//instructions: -4.4G (-6.52%)
✅ build/module/Mathlib.Algebra.Lie.Weights.Killing//instructions: -4.7G (-5.79%)
✅ build/module/Mathlib.Algebra.Lie.Weights.RootSystem//instructions: -6.5G (-10.54%)
✅ build/module/Mathlib.Algebra.Module.Injective//instructions: -3.4G (-10.93%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Polynomial//instructions: -4.8G (-12.56%)
✅ build/module/Mathlib.Algebra.Module.LocalizedModule.Basic//instructions: -7.2G (-7.41%)
✅ build/module/Mathlib.Algebra.Module.LocalizedModule.Submodule//instructions: -3.2G (-8.23%)
✅ build/module/Mathlib.Algebra.Module.SnakeLemma//instructions: -2.6G (-15.66%)
✅ build/module/Mathlib.Algebra.Module.ZLattice.Summable//instructions: -4.8G (-10.46%)
and 236 more

Small changes (853✅, 7🟥)

✅ build/lakeprof/longest build path//instructions: -507.6G (-11.20%)
✅ build/module/Aesop.Saturate//instructions: -499.7M (-3.48%)
✅ build/module/Aesop.Script.SpecificTactics//instructions: -786.1M (-9.05%)
✅ build/module/Aesop.Search.Expansion.Norm//instructions: -444.3M (-3.47%)
✅ build/module/Aesop.Search.Main//instructions: -347.6M (-3.45%)
✅ build/module/Aesop.Tree.ExtractScript//instructions: -397.1M (-6.99%)
✅ build/module/Mathlib.Algebra.AddConstMap.Basic//instructions: -1.6G (-6.88%)
✅ build/module/Mathlib.Algebra.Algebra.Bilinear//instructions: -2.0G (-12.94%)
✅ build/module/Mathlib.Algebra.Algebra.Equiv//instructions: -1.4G (-3.63%)
✅ build/module/Mathlib.Algebra.Algebra.Hom//instructions: -668.3M (-3.44%)
✅ build/module/Mathlib.Algebra.Algebra.Operations//instructions: -3.9G (-7.77%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Basic//instructions: -1.2G (-4.89%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Unitization//instructions: -1.4G (-6.44%)
✅ build/module/Mathlib.Algebra.Algebra.Tower//instructions: -1.3G (-6.32%)
✅ build/module/Mathlib.Algebra.Azumaya.Matrix//instructions: -1.4G (-9.00%)
✅ build/module/Mathlib.Algebra.BigOperators.Fin//instructions: -1.5G (-3.13%)
✅ build/module/Mathlib.Algebra.BigOperators.Finprod//instructions: -1.6G (-3.28%)
✅ build/module/Mathlib.Algebra.BigOperators.Finsupp.Basic//instructions: -1.7G (-6.03%)
✅ build/module/Mathlib.Algebra.BigOperators.Group.Finset.Basic//instructions: -983.9M (-2.07%)
✅ build/module/Mathlib.Algebra.Category.CommAlgCat.Monoidal//instructions: -2.2G (-2.79%)
and 840 more

Kha · 2026-07-30T19:41:26Z

!bench mathlib

leanprover-radar · 2026-07-30T19:42:42Z

Benchmark results for 14aa41f against 428f06e are in. There are significant results. @Kha

✅ build//instructions: -5.0T (-3.48%)

Large changes (40✅)

✅ build/module/Mathlib.Algebra.Group.Irreducible.Indecomposable//instructions: -7.2G (-19.42%)
✅ build/module/Mathlib.Algebra.Order.ToIntervalMod//instructions: -16.2G (-22.26%)
✅ build/module/Mathlib.Algebra.Star.NonUnitalSubalgebra//instructions: -24.6G (-24.14%)
✅ build/module/Mathlib.Analysis.Analytic.Basic//instructions: -39.4G (-34.59%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -17.1G (-36.81%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomialDef//instructions: -17.8G (-37.49%)
✅ build/module/Mathlib.Analysis.Analytic.Constructions//instructions: -39.1G (-33.39%)
✅ build/module/Mathlib.Analysis.Analytic.ConvergenceRadius//instructions: -17.2G (-31.94%)
✅ build/module/Mathlib.Analysis.Asymptotics.TVS//instructions: -16.4G (-24.19%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Basic//instructions: -15.6G (-24.09%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Defs//instructions: -39.5G (-36.63%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries//instructions: -33.9G (-28.20%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Operations//instructions: -39.6G (-35.01%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Mul//instructions: -16.7G (-20.89%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Add//instructions: -20.9G (-28.50%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Analytic//instructions: -24.4G (-20.45%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Basic//instructions: -15.7G (-25.94%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.CompCLM//instructions: -25.1G (-33.53%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap//instructions: -13.0G (-19.87%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Equiv//instructions: -13.0G (-23.04%)
and 19 more
and 1 hidden

Medium changes (232✅, 1🟥)

✅ build/module/Mathlib.Algebra.Algebra.NonUnitalHom//instructions: -3.9G (-14.93%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -10.1G (-15.55%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Quasispectrum//instructions: -3.0G (-9.30%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Rank//instructions: -3.7G (-29.86%)
✅ build/module/Mathlib.Algebra.Algebra.Unitization//instructions: -5.3G (-11.72%)
✅ build/module/Mathlib.Algebra.Exact.Basic//instructions: -2.5G (-6.74%)
✅ build/module/Mathlib.Algebra.FiveLemma//instructions: -2.8G (-13.63%)
✅ build/module/Mathlib.Algebra.Lie.Basis//instructions: -11.9G (-12.11%)
✅ build/module/Mathlib.Algebra.Lie.CartanExists//instructions: -3.1G (-10.23%)
✅ build/module/Mathlib.Algebra.Lie.Loop//instructions: -4.1G (-13.37%)
✅ build/module/Mathlib.Algebra.Lie.Weights.Cartan//instructions: -3.6G (-10.30%)
✅ build/module/Mathlib.Algebra.Lie.Weights.RootSystem//instructions: -6.2G (-9.96%)
✅ build/module/Mathlib.Algebra.Module.Injective//instructions: -3.2G (-10.48%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Polynomial//instructions: -4.6G (-12.12%)
✅ build/module/Mathlib.Algebra.Module.SnakeLemma//instructions: -2.5G (-15.06%)
✅ build/module/Mathlib.Algebra.Module.ZLattice.Summable//instructions: -4.5G (-9.84%)
✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -2.4G (-4.67%)
✅ build/module/Mathlib.Algebra.Order.Module.HahnEmbedding//instructions: -11.3G (-11.76%)
✅ build/module/Mathlib.Algebra.Order.Rearrangement//instructions: -2.9G (-12.99%)
✅ build/module/Mathlib.Algebra.Polynomial.Module.Basic//instructions: -5.6G (-13.75%)
and 213 more

Small changes (769✅, 8🟥)

✅ build/lakeprof/longest build path//instructions: -487.7G (-10.76%)
✅ build/module/Aesop.Saturate//instructions: -425.9M (-2.97%)
✅ build/module/Aesop.Script.SpecificTactics//instructions: -741.6M (-8.54%)
✅ build/module/Aesop.Search.Expansion.Norm//instructions: -384.6M (-3.01%)
✅ build/module/Aesop.Search.Main//instructions: -341.4M (-3.39%)
✅ build/module/Aesop.Tree.ExtractScript//instructions: -375.1M (-6.60%)
✅ build/module/Mathlib.Algebra.AddConstMap.Basic//instructions: -1.5G (-6.43%)
✅ build/module/Mathlib.Algebra.Algebra.Bilinear//instructions: -2.0G (-12.66%)
✅ build/module/Mathlib.Algebra.Algebra.Equiv//instructions: -1.3G (-3.28%)
✅ build/module/Mathlib.Algebra.Algebra.Operations//instructions: -3.5G (-6.97%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Basic//instructions: -1.1G (-4.58%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Unitization//instructions: -1.3G (-5.91%)
✅ build/module/Mathlib.Algebra.Algebra.Tower//instructions: -1.2G (-5.99%)
✅ build/module/Mathlib.Algebra.Azumaya.Matrix//instructions: -1.4G (-8.78%)
✅ build/module/Mathlib.Algebra.BigOperators.Fin//instructions: -1.3G (-2.61%)
✅ build/module/Mathlib.Algebra.BigOperators.Finprod//instructions: -1.4G (-2.88%)
✅ build/module/Mathlib.Algebra.BigOperators.Finsupp.Basic//instructions: -1.6G (-5.97%)
✅ build/module/Mathlib.Algebra.BigOperators.Group.Finset.Basic//instructions: -851.6M (-1.80%)
✅ build/module/Mathlib.Algebra.Category.CommAlgCat.Monoidal//instructions: -1.9G (-2.49%)
✅ build/module/Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf//instructions: -1.6G (-5.17%)
and 757 more

Kha · 2026-07-31T18:21:38Z

!bench mathlib

leanprover-radar · 2026-07-31T18:22:56Z

Benchmark results for 8dbb98d against 428f06e are in. There are significant results. @Kha

✅ build//instructions: -5.1T (-3.51%)

Large changes (40✅)

✅ build/module/Mathlib.Algebra.Group.Irreducible.Indecomposable//instructions: -7.2G (-19.48%)
✅ build/module/Mathlib.Algebra.Order.ToIntervalMod//instructions: -16.2G (-22.20%)
✅ build/module/Mathlib.Algebra.Polynomial.RuleOfSigns//instructions: -10.0G (-21.04%)
✅ build/module/Mathlib.Algebra.Star.NonUnitalSubalgebra//instructions: -24.6G (-24.20%)
✅ build/module/Mathlib.Analysis.Analytic.Basic//instructions: -39.4G (-34.58%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomial//instructions: -17.1G (-36.84%)
✅ build/module/Mathlib.Analysis.Analytic.CPolynomialDef//instructions: -17.7G (-37.47%)
✅ build/module/Mathlib.Analysis.Analytic.Constructions//instructions: -39.1G (-33.40%)
✅ build/module/Mathlib.Analysis.Analytic.ConvergenceRadius//instructions: -17.2G (-31.91%)
✅ build/module/Mathlib.Analysis.Asymptotics.TVS//instructions: -16.4G (-24.26%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Basic//instructions: -15.8G (-24.28%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Defs//instructions: -39.6G (-36.72%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries//instructions: -33.9G (-28.18%)
✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Operations//instructions: -39.6G (-35.02%)
✅ build/module/Mathlib.Analysis.Calculus.Deriv.Mul//instructions: -16.7G (-20.85%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Add//instructions: -20.9G (-28.41%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Analytic//instructions: -24.5G (-20.55%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Basic//instructions: -15.8G (-26.00%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.CompCLM//instructions: -25.1G (-33.51%)
✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Equiv//instructions: -13.0G (-23.07%)
and 19 more
and 1 hidden

Medium changes (230✅, 1🟥)

✅ build/module/Mathlib.Algebra.Algebra.NonUnitalHom//instructions: -3.9G (-14.98%)
✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -10.1G (-15.59%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Quasispectrum//instructions: -3.0G (-9.38%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Rank//instructions: -3.8G (-29.99%)
✅ build/module/Mathlib.Algebra.Algebra.Unitization//instructions: -5.4G (-11.88%)
✅ build/module/Mathlib.Algebra.Exact.Basic//instructions: -2.6G (-6.77%)
✅ build/module/Mathlib.Algebra.FiveLemma//instructions: -2.8G (-13.82%)
✅ build/module/Mathlib.Algebra.Lie.Basis//instructions: -12.0G (-12.15%)
✅ build/module/Mathlib.Algebra.Lie.CartanExists//instructions: -3.2G (-10.34%)
✅ build/module/Mathlib.Algebra.Lie.Loop//instructions: -4.1G (-13.39%)
✅ build/module/Mathlib.Algebra.Lie.Weights.Cartan//instructions: -3.6G (-10.25%)
✅ build/module/Mathlib.Algebra.Lie.Weights.RootSystem//instructions: -6.1G (-9.94%)
✅ build/module/Mathlib.Algebra.Module.Injective//instructions: -3.2G (-10.41%)
✅ build/module/Mathlib.Algebra.Module.LinearMap.Polynomial//instructions: -4.6G (-12.01%)
✅ build/module/Mathlib.Algebra.Module.SnakeLemma//instructions: -2.5G (-15.31%)
✅ build/module/Mathlib.Algebra.Module.ZLattice.Summable//instructions: -4.5G (-9.90%)
✅ build/module/Mathlib.Algebra.Order.Group.Pointwise.Interval//instructions: -2.5G (-4.90%)
✅ build/module/Mathlib.Algebra.Order.Module.HahnEmbedding//instructions: -11.3G (-11.77%)
✅ build/module/Mathlib.Algebra.Order.Rearrangement//instructions: -3.0G (-13.36%)
✅ build/module/Mathlib.Algebra.Polynomial.Module.Basic//instructions: -5.6G (-13.79%)
and 211 more

Small changes (779✅, 9🟥)

✅ build/lakeprof/longest build path//instructions: -495.5G (-10.93%)
✅ build/module/Aesop.Saturate//instructions: -432.7M (-3.01%)
✅ build/module/Aesop.Script.SpecificTactics//instructions: -747.3M (-8.61%)
✅ build/module/Aesop.Search.Expansion.Norm//instructions: -395.5M (-3.09%)
✅ build/module/Aesop.Search.Main//instructions: -343.1M (-3.40%)
✅ build/module/Aesop.Tree.ExtractScript//instructions: -385.7M (-6.79%)
✅ build/module/Mathlib.Algebra.AddConstMap.Basic//instructions: -1.5G (-6.44%)
✅ build/module/Mathlib.Algebra.Algebra.Bilinear//instructions: -1.9G (-12.35%)
✅ build/module/Mathlib.Algebra.Algebra.Equiv//instructions: -1.3G (-3.33%)
✅ build/module/Mathlib.Algebra.Algebra.Operations//instructions: -3.7G (-7.36%)
✅ build/module/Mathlib.Algebra.Algebra.Spectrum.Basic//instructions: -1.1G (-4.45%)
✅ build/module/Mathlib.Algebra.Algebra.Subalgebra.Unitization//instructions: -1.3G (-6.01%)
✅ build/module/Mathlib.Algebra.Algebra.Tower//instructions: -1.2G (-5.71%)
✅ build/module/Mathlib.Algebra.Azumaya.Matrix//instructions: -1.4G (-8.63%)
✅ build/module/Mathlib.Algebra.BigOperators.Fin//instructions: -1.3G (-2.65%)
✅ build/module/Mathlib.Algebra.BigOperators.Finprod//instructions: -1.5G (-2.99%)
✅ build/module/Mathlib.Algebra.BigOperators.Finsupp.Basic//instructions: -1.7G (-6.30%)
✅ build/module/Mathlib.Algebra.BigOperators.Group.Finset.Basic//instructions: -853.2M (-1.80%)
✅ build/module/Mathlib.Algebra.Category.CommAlgCat.Monoidal//instructions: -1.9G (-2.45%)
✅ build/module/Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf//instructions: -1.6G (-5.22%)
and 768 more

downstream: follow upstream PR

19e564b

downstream-lean4 Bot added the adaptation This is an adaptation PR for a PR in the lean4 repository. label Jul 24, 2026

downstream-lean4 Bot mentioned this pull request Jul 24, 2026

perf: normalize free variables in the type class resolution cache key leanprover/lean4#14369

Draft

downstream-lean4 Bot added the toolchain-available label Jul 24, 2026

downstream-lean4 Bot removed the toolchain-available label Jul 24, 2026

downstream: follow upstream PR

f519b24

downstream-lean4 Bot added toolchain-available and removed toolchain-available labels Jul 24, 2026

downstream: follow upstream PR

73ebb47

downstream-lean4 Bot added toolchain-available and removed toolchain-available labels Jul 26, 2026

downstream: follow upstream PR

c1515c8

downstream-lean4 Bot added the toolchain-available label Jul 26, 2026

Kha removed the toolchain-available label Jul 28, 2026

downstream: follow upstream PR

e0da297

downstream-lean4 Bot added the toolchain-available label Jul 28, 2026

Kha removed the toolchain-available label Jul 28, 2026

downstream: follow upstream PR

4eb9917

downstream-lean4 Bot added the toolchain-available label Jul 28, 2026

Kha removed the toolchain-available label Jul 29, 2026

downstream: follow upstream PR

de38a79

downstream-lean4 Bot added the toolchain-available label Jul 29, 2026

Kha removed the toolchain-available label Jul 30, 2026

downstream: follow upstream PR

14aa41f

downstream-lean4 Bot added the toolchain-available label Jul 30, 2026

Kha removed the toolchain-available label Jul 31, 2026

downstream: follow upstream PR

8dbb98d

downstream-lean4 Bot added the toolchain-available label Jul 31, 2026

downstream-lean4 Bot removed the toolchain-available label Aug 9, 2026

downstream: follow upstream PR

bb91010

downstream-lean4 Bot added toolchain-available and removed toolchain-available labels Aug 9, 2026

Uh oh!

Conversation

downstream-lean4 Bot commented Jul 24, 2026

Uh oh!

Kha commented Jul 24, 2026

Uh oh!

leanprover-radar commented Jul 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-radar commented Jul 24, 2026

Uh oh!

downstream-lean4 Bot commented Jul 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Build report for downstream: follow upstream PR

Uh oh!

Kha commented Jul 24, 2026

Uh oh!

leanprover-radar commented Jul 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Kha commented Jul 26, 2026

Uh oh!

leanprover-radar commented Jul 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Kha commented Jul 26, 2026

Uh oh!

leanprover-radar commented Jul 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Kha commented Jul 28, 2026

Uh oh!

leanprover-radar commented Jul 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Kha commented Jul 28, 2026

Uh oh!

leanprover-radar commented Jul 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Garmelon commented Jul 28, 2026

Uh oh!

leanprover-radar commented Jul 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Garmelon commented Jul 28, 2026

Uh oh!

Kha commented Jul 29, 2026

Uh oh!

leanprover-radar commented Jul 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Kha commented Jul 30, 2026

Uh oh!

leanprover-radar commented Jul 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Kha commented Jul 31, 2026

Uh oh!

leanprover-radar commented Jul 31, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

leanprover-radar commented Jul 24, 2026 •

edited

Loading

downstream-lean4 Bot commented Jul 24, 2026 •

edited

Loading

leanprover-radar commented Jul 24, 2026 •

edited

Loading

leanprover-radar commented Jul 26, 2026 •

edited

Loading

leanprover-radar commented Jul 26, 2026 •

edited

Loading

leanprover-radar commented Jul 28, 2026 •

edited

Loading

leanprover-radar commented Jul 28, 2026 •

edited

Loading

leanprover-radar commented Jul 28, 2026 •

edited

Loading

leanprover-radar commented Jul 29, 2026 •

edited

Loading

leanprover-radar commented Jul 30, 2026 •

edited

Loading

leanprover-radar commented Jul 31, 2026 •

edited

Loading